#include "alter.h"
#include "functions.h"
#include "parse_tree_def.h"
#include <stdio.h>
#include <stdlib.h>

int main()
{
    try
    {
        freopen("E:/codes/courses/ArtificialIntelligence/CNF/out.txt", "w", stdout);
        string s = " (	(	( @x)(P(x,y)>(Q(x)!R(y))) % (@x)(#y)(P(x,y)!~Q(z))	)	>R(y) )";
        // string s = "(   (@x)(P(x,y) >   (R(x)!~W(x)))>   Q(y)   )";
        erase_space_tab(s); //清除空格、\t
        node *root = new node();
        char *head = (char *)s.data();
        try
        {
            root = splay(root, head);
        }
        catch (ParseError &s)
        {
            switch (s.type)
            {
            case ERR_BADFMT:
                printf("公式中格式错误，请检查");
                break;
            case ERR_UNRECG:
                printf("公式在第%d个字符附近无法识别", g_peek - g_head + 1);
            default:
                break;
            }
            exit(0);
        }
        hierarchical_traverse(root, show_lr);

        elim_conds(root);

        hierarchical_traverse(root, show_lr);

        reduce_nega_scope(root);

        hierarchical_traverse(root, show_lr);

        standardize_vars(root);

        hierarchical_traverse(root, show_lr);

        erase_exsits(root);

        hierarchical_traverse(root, show_lr);

        erase_allqunt(root);

        hierarchical_traverse(root, show_lr);
    }
    catch (ParseError s)
    {
        //异常处理
    }
}